docs: proof-reading the tutorial #2636
Conversation
|
BTW @andreasabel, thanks for reminding me! This has been collecting dust for... turns out, exactly a year. I was initially meaning to go over all readme modules; alas, that hadn't happened. Uneasy times. |
There was a problem hiding this comment.
Thanks for offering this. I think it would be good to nail down the discussion with @Taneb before merging, though.
There was a problem hiding this comment.
Suggest rewriting (rather than deleting) the paragraph in favour of (some version of) the suggestion below.
Either that, or reinstate the paragraph and we can have another go as a separate PR (but that seems 'wasteful', given that the one at hand already problematises the paragraph as needing fixing in some for or another...)
|
Six weeks later, let me ask explicitly again for comments on my proposed rephrasing... |
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
|
Sorry for the long reply time, yes that rephrasing sounds fine to me @jamesmckinna, thanks for suggesting! |
|
Thanks @MatthewDaggitt ... paragraph (tweaked) now committed. |
jamesmckinna
dismissed
their stale review
I've now committed my originally suggested paragraph, with some subsequent (typographic) tweaks
|
If one of us can (re-)read what is now there, suggest we merge? |
|
Thanks for the tweaks @ulidtko and @jamesmckinna, merging in now. |
Hi, Agda team!
Here's a small patch in the tutorial,
doc/README*, with minor editorials: typos and the like.I know it's always easier for (somebody else's) fresh set of eyeballs to do proof-reads. Thus, here goes.
Hoping for easy merge — there's no code change, just the docstrings.